Size collections from the instance passed to NewTheorem - #93

Fixes #78.

The defect

A collection symbol takes its length from the collection already on the solution instance, and
read it with no null check:

private sealed class Env { public int[]? Values { get; set; } }   // no initialiser

using var ctx = new Z3Context();
ctx.NewTheorem<Env>().Solve();
// System.NullReferenceException: Object reference not set to an instance of an object.

Two halves, as the issue puts it. The diagnostic half: a forgettable mistake produced a bare
NRE with nothing naming the member - in an environment with several collections, nothing said
which. The structural half: a value tuple could never hold a collection at all, because the
instance is built with Activator.CreateInstance and a tuple has nowhere to put an initialiser.
Nothing the caller could write fixed that.

Measured before the change: a null field, a null property, a null List<T>, a null collection on
a nested object, and a tuple - with or without element constraints - all threw the same bare NRE.

The change

The instance passed to NewTheorem(T) is now the template for the solution. That overload
already existed; its parameter was named dummy and the method discarded it. Its collections
now give the solution's collections their length, so:

ctx.NewTheorem((Values: new int[2], Other: 0))
   .Where(t => t.Values[0] == 3)
   .Where(t => t.Values[1] == 4)
   .Solve();                                  // (Values: [3, 4], Other: ...)

works, and so does an anonymous type with a collection - which #75 had to refuse by name two PRs
ago, for exactly the reason this fixes: the anonymous instance is created uninitialised, and the
initialised one the caller passed was being thrown away.

Rules, each pinned by a test and a mutation:

• The template beats the type's own initialiser. The caller who passes an instance has said what
  they want more directly than the type has. With no template, the initialiser applies as before.
• The template is followed into nested objects: the recursion carries the corresponding member
  of the template alongside the environment.
• It survives Where (each of which builds a new theorem) and reaches the optimiser, so
  OrderBy sees it.
• Only lengths are read. The template's element values do not reach the solution, and the
  template is never written to.
• A collection with no length from either source is rejected by name:
  Collection symbol B has no length. A collection must be pre-sized: initialise it on the environment type, or pass an instance with it initialised to NewTheorem.

The //todo: deal with length in a more robust way that sat above the count read for years is
gone with it.

Public surface

Z3Context.NewTheorem<T>(T dummy) becomes NewTheorem<T>(T template) and reads the argument.
Binary-compatible; source-breaking only for a caller using the named argument dummy:. The XML
documentation on the overload is rewritten to say what the instance is for, with a tuple example
beside the anonymous-type one.

This was put to the maintainer against the diagnostic-only fix the issue suggested as the safe
minimum, with the measurements above, and chosen.

Tests

239 → 247. Three pins rewritten in CollectionSymbolTests, one in EnvironmentTypeTests, and
new coverage for each rule.

Mutation results

Verification

• dotnet build solutions/Z3.Linq.slnx -c Release - clean, TreatWarningsAsErrors on
• 247/247 locally
• ./build.ps1 -Configuration Release - 46 tasks, 0 errors, 0 warnings
• Coverage 88.5% -> 88.1% line (693 of 786) and 77.2% -> 77.5% branch (459 of 592). Eight more coverable lines, four of them covered: the uncovered four are the two constructor overloads that keep the old signatures and the unreachable default arm of the new member-reading helper

Release note

Releases remain on hold under #60 until Microsoft.Z3 5.x reaches nuget.org, so this reaches main
but not consumers. Nothing about the hold changes.